Inference at * 1 2 
Iof proof for Lemma eq int eq true elim sqequal:

.....wf..... NILNIL

1. i : 
2. j : 
  ((i = j) ~ tt)  Type 

latex

 by MemCD 

latex

 1: .....subterm..... T:t1:n

 1:   (i = j) ~ (i = j)
 2: .....subterm..... T:t2:n

 2:   tt ~ tt
 .

Definitions	t  T
Lemmas	int sq